poss:(ES{i}{i'}), T:Type{i}, s:T, i:Id, P, Q:(possible-event{i:l}(poss){i'}).
(e:possible-event{i:l}(poss). (P(e))  (Q(e)))
 (R:(possible-event{i:l}(poss)possible-event{i:l}(poss){i'}), Rs:(TT{i'}).
 ma-knows{i:l}(poss; i; T; s; P; Rs; R)  ma-knows{i:l}(poss; i; T; s; Q; Rs; R)) 

latex

Definitions	t  T, P  Q, x:A. B(x), x:A  B(x), PossibleEvent(poss), A c B, poss-consistent(i;T;s;ev;R), K(P)@e, Type, , ES, x:AB(x), Id, f(a), Atom$n, Ki(P)@s
Lemmas	poss-consistent wf, es-knows wf, possible-event wf, Id wf, event system wf, es-knows-trans